(set-info :smt-lib-version 2.6)
(set-logic QF_BV)
(set-info :source |
Ivan Jager <aij+nospam@andrew.cmu.edu>

|)
(set-info :category "industrial")
(set-info :status sat)
(declare-fun t_339 () (_ BitVec 1))
(declare-fun t_338 () (_ BitVec 1))
(declare-fun t_337 () (_ BitVec 1))
(declare-fun t_336 () (_ BitVec 1))
(declare-fun t_335 () (_ BitVec 1))
(declare-fun t_334 () (_ BitVec 1))
(declare-fun t_333 () (_ BitVec 1))
(declare-fun t_332 () (_ BitVec 1))
(declare-fun t_331 () (_ BitVec 1))
(declare-fun t_330 () (_ BitVec 1))
(declare-fun t_329 () (_ BitVec 1))
(declare-fun t_328 () (_ BitVec 1))
(declare-fun t_327 () (_ BitVec 1))
(declare-fun t_326 () (_ BitVec 1))
(declare-fun t_325 () (_ BitVec 1))
(declare-fun t_324 () (_ BitVec 1))
(declare-fun t_323 () (_ BitVec 1))
(declare-fun t_322 () (_ BitVec 1))
(declare-fun t_321 () (_ BitVec 1))
(declare-fun t_320 () (_ BitVec 1))
(declare-fun t_319 () (_ BitVec 1))
(declare-fun t_318 () (_ BitVec 1))
(declare-fun t_317 () (_ BitVec 1))
(declare-fun t_316 () (_ BitVec 1))
(declare-fun t_315 () (_ BitVec 1))
(assert (= (_ bv1 1) (bvand (bvand (bvand (bvand (bvand (bvand (bvand (bvand (bvand (bvand (bvand (bvand (bvand (bvand (bvand (bvand (bvand (bvand (bvand (bvand (bvand (bvand (bvand (bvand (bvand (ite (= t_339 (bvand t_338 (_ bv1 1))) (_ bv1 1) (_ bv0 1)) (ite (= t_338 (bvand t_337 (_ bv1 1))) (_ bv1 1) (_ bv0 1))) (ite (= t_337 (bvand t_336 (_ bv1 1))) (_ bv1 1) (_ bv0 1))) (ite (= t_336 (bvand t_335 (_ bv1 1))) (_ bv1 1) (_ bv0 1))) (ite (= t_335 (bvand t_334 (_ bv1 1))) (_ bv1 1) (_ bv0 1))) (ite (= t_334 (bvand t_333 (_ bv1 1))) (_ bv1 1) (_ bv0 1))) (ite (= t_333 (bvand t_332 (_ bv1 1))) (_ bv1 1) (_ bv0 1))) (ite (= t_332 (bvand t_331 (_ bv1 1))) (_ bv1 1) (_ bv0 1))) (ite (= t_331 (bvand t_330 (_ bv1 1))) (_ bv1 1) (_ bv0 1))) (ite (= t_330 (bvand t_329 (_ bv1 1))) (_ bv1 1) (_ bv0 1))) (ite (= t_329 (bvand t_328 (_ bv1 1))) (_ bv1 1) (_ bv0 1))) (ite (= t_328 (bvand t_327 (_ bv1 1))) (_ bv1 1) (_ bv0 1))) (ite (= t_327 (bvand t_326 (_ bv1 1))) (_ bv1 1) (_ bv0 1))) (ite (= t_326 (bvand t_325 (_ bv1 1))) (_ bv1 1) (_ bv0 1))) (ite (= t_325 (bvand t_324 (_ bv1 1))) (_ bv1 1) (_ bv0 1))) (ite (= t_324 (bvand t_323 (_ bv1 1))) (_ bv1 1) (_ bv0 1))) (ite (= t_323 (bvand t_322 (_ bv1 1))) (_ bv1 1) (_ bv0 1))) (ite (= t_322 (bvand t_321 (_ bv1 1))) (_ bv1 1) (_ bv0 1))) (ite (= t_321 (bvand t_320 (_ bv1 1))) (_ bv1 1) (_ bv0 1))) (ite (= t_320 (bvand t_319 (_ bv1 1))) (_ bv1 1) (_ bv0 1))) (ite (= t_319 (bvand t_318 (_ bv1 1))) (_ bv1 1) (_ bv0 1))) (ite (= t_318 (bvand t_317 (_ bv1 1))) (_ bv1 1) (_ bv0 1))) (ite (= t_317 (bvand t_316 (_ bv1 1))) (_ bv1 1) (_ bv0 1))) (ite (= t_316 (bvand t_315 (_ bv1 1))) (_ bv1 1) (_ bv0 1))) (ite (= t_315 (_ bv1 1)) (_ bv1 1) (_ bv0 1))) (bvand (bvnot (_ bv0 1)) (bvor (bvnot (bvand t_339 (_ bv1 1))) (_ bv1 1))))))
(check-sat)
(exit)
